import java.util.List;
import java.util.Map;

/**
 * 
 * @author "Cunxin Jia"
 *
 */
public class Literal implements Comparable<Literal>{
	private Atom atom;
	private boolean isNegative;
	
	public Literal(String literalString) {
		if(literalString.charAt(0) == '~') {
			isNegative = true;
			atom = new Atom(literalString.substring(1));
		}
		else {
			isNegative = false;
			atom = new Atom(literalString);
		}
	}
	
	/**
	 * Substitute variables with constants
	 * @param substitution
	 */
	public Literal substitute(Map<Term,Term> substitution) {
		Literal newLiteral = this;
		List<Term> terms = newLiteral.getAtom().getTerms();
		for(int i = 0; i < terms.size(); i++) {
			Term curTerm = terms.get(i);
			if(curTerm.isConstant() == false) {
				Term newTerm = substitution.get(curTerm);
				newLiteral.getAtom().substitute(i, newTerm);
			}
		}
		return newLiteral;
	}
	
	/**
	 * 
	 * Notice: this method can be optimised
	 * @return true if the clause is ground
	 */
	public boolean isGround() {
		List<Term> terms = atom.getTerms();
		for(int i = 0; i < terms.size(); i++) {
			Term curTerm = terms.get(i);
			if(!curTerm.isConstant()) {
				return false;
			}
		}
		return true;
	}
	
	
	public Literal(Atom atom, boolean isNegative) {
		this.atom = atom;
		this.isNegative = isNegative;
	}
	
	public boolean isNegative() {
		return isNegative;
	}
	
	public boolean isPositive() {
		return !isNegative;
	}
	
	public Atom getAtom() {
		return atom;
	}
	
	public String toString() {
		if(isNegative) {
			return "~" + atom.toString();
		}
		else {
			return atom.toString();
		}
	}
	
	@Override
	public boolean equals(Object o) {
		if(toString().equals(o.toString()))
			return true;
		else
			return false;
	}
	
	@Override
	public int hashCode() {
		return toString().hashCode();
	}

	@Override
	public int compareTo(Literal o) {
		return this.toString().compareTo(o.toString());
	}
}
